A:Type, eq:EqDecider(A), f:a:A fp Top, L:A List.
l_disjoint(A;1of(f);L)  (a:A. a  dom(f)  (a  L)) 

latex

Definitions	a:A fp B(a), l_disjoint(T;l1;l2), x  dom(f), P  Q, P  Q, False, P & Q, P  Q, Prop, b, deq-member(eq;x;L), 1of(t), x. t(x), A, (x  l), Top, EqDecider(T), x:A. B(x), t  T
Lemmas	assert-deq-member, deq wf, top wf, l member wf, not wf, pi1 wf, deq-member wf, assert wf